the_es:ES, e, e':E. ((e <loc e') & (e1:E. ((e <loc e1) & (e1 <loc e'))))  (e = pred(e')) 

latex

Definitions	x:A. B(x), P  Q, P & Q, A c B, t  T, , A, P  Q, P  Q, P  Q, False
Lemmas	es-axioms, es-locl wf, es-E wf, not wf, event system wf, assert wf, es-first wf, es-pred wf, Id wf, es-loc wf, es-loc-pred